($\lambda$$A$,$l$,$z$. $\parallel$$l$$\parallel$) $\in$ $A$:Type$\rightarrow$($A$ List)$\rightarrow\downarrow$True$\rightarrow\mathbb{Z}$